/*
 * LPB.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/LPB.hpp"

#include <algorithm>
#include <string>
#include <vector>
#include <sstream>
#include <iostream>
#include <list>

#include "bfr/Literal.hpp"
#include "bfr/CoefficientType.hpp"
#include "bfr/Clause.hpp"
#include "bfr/ClauseSet.hpp"

using std::list;

namespace bfr {

LPB::LPB(const lpb_coefficient_t d, const size_t initial_size)
: degree(d), summands() {
    summands.reserve(initial_size);
}

LPB::LPB(const LPB &other)
: degree(other.degree), summands(other.summands) { }

LPB::~LPB() { }


std::ostream& operator<<(std::ostream &out, const LPB &l) {
    if (l.size() == 0) {
        out << '0';
    }
    else {
        bool first = true;
        for (size_t i = 0; i < l.summands.size(); i++) {
            if(first)
                first = false;
            else
                out << " + ";
            out << l.summands[i];
        }
    }
    out << " >= " << l.degree;
    return out;
}

std::string LPB::asString() const {
    std::ostringstream stream;
    stream << *this;
    return stream.str();
}

void LPB::addSummand(lpb_coefficient_t coefficient,
        const Literal &literal) {
    LPBSummand s(coefficient, literal);
    // check if vector is big enough
    // otherwise the vector will expand
    size_t id = literal.getId();
    if(summands.size() > id) {
        summands[id] = s;
    }
    else {
        summands.reserve(id);
        // finally put it to it's right location
        // if the vector is not "full" add some dummies
        for(size_t i = summands.size(); i < id; ++i) {
            summands.push_back(LPBSummand(-1, Literal(-1)));
        }
        summands.push_back(s);
    }
}

const LPBSummand& LPB::operator[](size_t index) const {
    return summands[index];
}

lpb_coefficient_t LPB::getDegree() const {
    return degree;
}

size_t LPB::size() const {
    return summands.size();
}

void LPB::sortCoefficients() {
    std::sort(summands.begin(), summands.end(),
            LPBSummand::CompareEntriesG());
}

ClauseSet* LPB::toDNF() const {
    ClauseSet *result = new ClauseSet();
    lpb_coefficient_t sum = 0;
    for (size_t i = 0; i < summands.size(); i++) {
        sum += summands[i].getCoefficient();
    }
    if (sum < degree) {
        // represents false
        return result;
    }

    // work now on a copy
    LPB copy(*this);
    copy.sortCoefficients();
    if (degree <= 0) {
        // represents true
        Clause *emptyClause = new Clause();
        result->addSecure(emptyClause);
        return result;
    }

    struct SetValuePair {
            list<Literal> literals;
            lpb_coefficient_t sum;
            size_t nextIndex;

            explicit SetValuePair(const SetValuePair &other)
            : literals(other.literals), sum(other.sum),
              nextIndex(other.nextIndex) { }

            explicit SetValuePair(size_t nI, lpb_coefficient_t s=0)
            : literals(), sum(s), nextIndex(nI) { }

    };

    SetValuePair empty(0);
    list<SetValuePair> incompleteClauses;

    incompleteClauses.push_back(empty);

    while (!incompleteClauses.empty()) {
        SetValuePair &next = incompleteClauses.front();

        if (next.sum >= degree) {
            Clause *clause = new Clause(next.literals.size());
            while (!next.literals.empty()) {
                clause->add(Literal(next.literals.front()));
                next.literals.pop_front();
            }
            result->addSecure(clause);
        }
        else {
            size_t nextInd = next.nextIndex;
            for (size_t i = nextInd; i < size(); i++) {
                SetValuePair newPair(next);
                newPair.nextIndex = i + 1;
                newPair.sum = next.sum + copy.summands[i].getCoefficient();
                newPair.literals.push_back(copy.summands[i].getLiteral());
                incompleteClauses.push_back(newPair);
            }
        }
        incompleteClauses.pop_front();
    }
    return result;
}

} // namespace bfr
